d-partial-world(D;f;t';s)
== <(i,x. M(i).ds(x))
== ,(i,a. M(i).da(locl(a)))
== ,(l,tg. M(source(l)).dout(l,tg))
== ,(i,t. if t<t' 1of(f(t,i)) else s(i) fi)
== ,(i,t. if t<t' 1of(2of(f(t,i))) else null fi)
== ,(i,t. if t<t' 2of(2of(f(t,i))) else nil fi)
== ,(i.NullMachine)
== ,> 

latex

---

clarification:

d-partial-world(D;f;t';s)
== <(i,x. d-m(D; i).ds(x))
== ,(i,a. d-m(D; i).da(locl(a)))
== ,(l,tg. d-m(D; source(l)).dout(l,tg))
== ,(i,t. if t<t' 1of(f(t,i)) else s(i) fi)
== ,(i,t. if t<t' 1of(2of(f(t,i))) else null fi)
== ,(i,t. if t<t' 2of(2of(f(t,i))) else nil fi)
== ,(i.NullMachine)
== ,> 

latex

Definitions	M.ds(x), M.da(a), locl(a), M.dout(l,tg), M(i), source(l), 1of(t), null, if b t else f fi, i<j, 2of(t), f(a), nil, <a,b>, x.A(x),
FDL editor aliases	d-partial-world